/-
Copyright (c) 2025 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.CategoryTheory.Elements
import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

/-!
# The preordered type of simplices of a simplicial set

In this file, we define the type `X.S` of simplices of a simplicial set `X`,
where a simplex consists of the data of `dim : ℕ` and `simplex : X _⦋dim⦌`.
We endow this type with a preorder defined by
`x ≤ y ↔ Subcomplex.ofSimplex x.simplex ≤ Subcomplex.ofSimplex y.simplex`.
In particular, as a preordered type, `X.S` is a category, but this is
not what is called "the category of simplices of `X`" in the literature
(and which is `X.Elementsᵒᵖ` in mathlib).

## TODO (@joelriou)

* Extend the `S` structure to define the type of nondegenerate
simplices of a simplicial set `X`, and also the type of nondegenerate
simplices of a simplicial set `X` which do not belong to a given subcomplex.

-/

universe u

open CategoryTheory Simplicial

namespace SSet

variable (X : SSet.{u})

/-- The type of simplices of a simplicial set `X`. This type `X.S` is in bijection
with `X.Elements` (see `SSet.S.equivElements`), but `X.S` is not what the literature
names "category of simplices of `X`", as the category on `X.S` comes from
a preorder (see `S.le_iff_nonempty_hom`). -/
structure S where
  /-- the dimension of the simplex -/
  {dim : ℕ}
  /-- the simplex -/
  simplex : X _⦋dim⦌

variable {X}

namespace S

lemma mk_surjective (s : X.S) :
    ∃ (n : ℕ) (x : X _⦋n⦌), s = mk x :=
  ⟨s.dim, s.simplex, rfl⟩

/-- The image of a simplex by a morphism of simplicial sets. -/
def map {Y : SSet.{u}} (f : X ⟶ Y) (s : X.S) : Y.S :=
  S.mk (f.app _ s.simplex)

lemma dim_eq_of_eq {s t : X.S} (h : s = t) :
    s.dim = t.dim :=
  congr_arg dim h

lemma dim_eq_of_mk_eq {n m : ℕ} {x : X _⦋n⦌} {y : X _⦋m⦌}
    (h : S.mk x = S.mk y) : n = m :=
  dim_eq_of_eq h

section

variable (s : X.S) {d : ℕ} (hd : s.dim = d)

/-- When `s : X.S` is such that `s.dim = d`, this is a term
that is equal to `s`, but whose dimension if definitionally equal to `d`. -/
@[simps dim]
def cast : X.S where
  dim := d
  simplex := _root_.cast (by simp only [hd]) s.simplex

lemma cast_eq_self : s.cast hd = s := by
  obtain ⟨d, _, rfl⟩ := s.mk_surjective
  obtain rfl := hd
  rfl

@[simp]
lemma cast_simplex_rfl : (s.cast rfl).simplex = s.simplex := rfl

end

lemma ext_iff' (s t : X.S) :
    s = t ↔ ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex :=
  ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun ⟨h₁, h₂⟩ ↦ by
    obtain ⟨_, _, rfl⟩ := s.mk_surjective
    obtain ⟨_, _, rfl⟩ := t.mk_surjective
    aesop⟩

lemma ext_iff {n : ℕ} (x y : X _⦋n⦌) :
    S.mk x = S.mk y ↔ x = y := by
  simp

/-- The subcomplex generated by a simplex. -/
abbrev subcomplex (s : X.S) : X.Subcomplex := Subcomplex.ofSimplex s.simplex

/-- If `s : X.S` and `t : X.S` are simplices of a simplicial set, `s ≤ t` means
that the subcomplex generated by `s` is contained in the subcomplex generated by `t`,
see `SSet.S.le_def` and `SSet.S.le_iff`. Note that the
category structure on `X.S` induced by this preorder is not
the "category of simplices" of `X` (which is see `X.Elementsᵒᵖ`);
see `SSet.S.le_iff_nonempty_hom` for the precise relation. -/
instance : Preorder X.S := Preorder.lift subcomplex

lemma le_def {s t : X.S} : s ≤ t ↔ s.subcomplex ≤ t.subcomplex :=
  Iff.rfl

lemma le_iff {s t : X.S} :
    s ≤ t ↔ ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌), X.map f.op t.simplex = s.simplex := by
  rw [le_def, Subcomplex.ofSimplex_le_iff, Subpresheaf.ofSection_obj, Set.mem_setOf_eq]
  tauto

lemma mk_map_le {n m : ℕ} (x : X _⦋n⦌) (f : ⦋m⦌ ⟶ ⦋n⦌) :
    S.mk (X.map f.op x) ≤ S.mk x := by
  rw [le_iff]
  tauto

lemma mk_map_eq_iff_of_mono {n m : ℕ} (x : X _⦋n⦌)
    (f : ⦋m⦌ ⟶ ⦋n⦌) [Mono f] :
    S.mk (X.map f.op x) = S.mk x ↔ IsIso f := by
  constructor
  · intro h
    obtain rfl := S.dim_eq_of_mk_eq h
    obtain rfl := SimplexCategory.eq_id_of_mono f
    infer_instance
  · intro hf
    obtain rfl := SimplexCategory.eq_of_isIso f
    obtain rfl := SimplexCategory.eq_id_of_isIso f
    simp

/-- The type of simplices of `X : SSet.{u}` identifies to the type
of elements of `X` considered as a functor `SimplexCategoryᵒᵖ ⥤ Type u`.
(Note that this is not an (anti)equivalence of categories,
see `S.le_iff_nonempty_hom`.) -/
@[simps!]
def equivElements : X.S ≃ X.Elements where
  toFun s := X.elementsMk _ s.simplex
  invFun := by
    rintro ⟨⟨n⟩, x⟩
    induction n using SimplexCategory.rec
    exact S.mk x
  left_inv _ := rfl
  right_inv _ := rfl

lemma le_iff_nonempty_hom (x y : X.S) :
    x ≤ y ↔ Nonempty (equivElements y ⟶ equivElements x) := by
  rw [le_iff]
  constructor
  · rintro ⟨f, hf⟩
    exact ⟨⟨f.op, hf⟩⟩
  · rintro ⟨f, hf⟩
    exact ⟨f.unop, hf⟩

end S

end SSet
